Switches and routers generally operate by indexing into a forwarding table using a destination address and deciding where to send a received packet. In recent years, such forwarding has grown more complicated. Middle boxes (e.g., network address translators (NATs) and firewalls) and encapsulation mechanisms (e.g., virtual local area networks (VLANs) and multiprotocol label switching (MPLS) devices) have been developed to escape some of the limitations of internet protocol (IP). For example, NAT bypasses address limits and MPLS allows flexible routing. Further, new protocols for specific domains, such as data centers, wide area networks (WANs) and wireless, have greatly increased the complexity of packet forwarding. Today, there are over 6,000 Internet Requests for Comment (RFCs) and it is not unusual for a switch or router to handle ten or more encapsulation formats simultaneously.
This complexity makes it increasingly difficult to operate a large network. Network operators require great sophistication to master the complexity of many interacting protocols and middle boxes. The complexity makes network operators wary of trying new protocols, even if they are available, for fear of breaking their network. Complexity also makes networks fragile, and susceptible to problems where hosts become isolated and unable to communicate. Moreover, debugging reachability problems is very time consuming. Even simple questions such as “Can Host A talk to Host B?” or “Can packets loop in my network?” or “Can User A listen to communications between Users B and C?” are difficult to answer. These questions are especially hard to answer in networks carrying multiple encapsulations and containing boxes that filter packets.
The process of forwarding packets is prone to faults from configuration errors and unexpected protocol interactions. In large packet networks, forwarding tables in routers/switches are updated by multiple protocols. Access control lists (ACLs) in routers, switches, and firewalls are designed and configured by different people over a long period of time. Links may be physical or virtual (e.g., VLAN, MPLS). Some middle boxes also modify packets (e.g., NAT). For at least these reasons, despite being mission-critical for most organizations, managing a network is surprisingly difficult.
In large scale data centers, protocol changes are frequent and operators usually do not have a full picture of the network. The result is common and expensive misconfigurations. Given a set of high level requirements (e.g., reachability, security), network operators need to precisely understand:
(i) the behavior of the protocols (often distributed);
(ii) how the protocols interact with each other; and
(iii) how each parameter in the configuration affects the distributed computation.
The network operators then manually figure out the individual configurations of potentially hundreds of devices running complex distributed protocols so that they may compute a forwarding state compatible to high level requirements. Because of this complexity, network operators often make mistakes that can lead to severe network downtimes. Indeed, studies show that most network downtimes are caused by humans, not equipment failures.
Also, network state may change rapidly in response to customer demands, load conditions, or configuration changes. For example, networks are subject to dynamic state changes over time as a result of rule insertion and deletion by protocols and operators, failure and recovery of links and boxes, etc. Network status is read and network atomic flows are generated based on different types of rules. As used herein, data packets in the same atomic flow or equivalence class (EC) have the same behavior in the network. Existing systems address these issues by separating the forwarding table and the ACL and by reducing redundancy in the forwarding table and the ACL. The network must also ensure correctness conditions such as isolating tenants from each other and from critical services. However, existing policy checkers cannot verify compliance in real-time because of the need to collect “state” from the entire network and the time it takes to analyze this state.
As computer networks become more and more complex, an automatic network review tool that takes the network's forwarding state as input, summarizes the overall state, and generates some general reports about the reachability relationship, the key point, the duplicated routes, or back-up routes of the network becomes increasingly desirable. Also, when network operators need to switch the configuration of a network into a new configuration, a general difference report of the two configurations is desirable for facilitating the configuration changes. It is further desirable that the network analyzing tool also strengthen the operator's capability to better administer the network.
Existing network verification or analysis methods mainly focus on single point analysis and verification. Few network verification or analysis methods evaluate the network as a whole and provide an overall “review” function. Those network verification or analysis methods that do provide whole network analysis functionality do so by traversing all possible node pairs or paths and verifying them one by one, which costs lots of time and space.
A system identified as Veriflow is described by Khurshid et al. in “Veriflow: Verifying Network-Wide Invariants in Real Time,” in HotSDN, 2012, purports to provide a layer between a software-defined networking controller and network devices to check for network-wide invariant solutions dynamically in real-time as each forwarding rule is inserted, modified, or deleted. By checking each change to forwarding behavior before it takes effect, Veriflow purports to block changes that may violate important invariants (e.g., prohibit changes that violate access control policies or cause forwarding loops).
Veriflow uses the approach of data plane verification since the data-plane state has relatively simple formats and semantics that are common across many higher-layer protocols and implementations and thus simplifies rigorous analysis of a network. In routing, the data plane defines the part of the router architecture that decides what to do with packets arriving on an inbound interface. Generally, the data plane refers to a table in which the router looks up the destination address of the incoming packet and retrieves the rules and other information necessary to determine the path from the receiving element, through the routing device, and to the proper outgoing interface. Depending upon the router implementation, the table in which the destination is looked up could be the routing table (or routing information base (RIB)) or a separate forwarding information base (FIB) that is loaded by the routing control plane but used by the data plane for higher speed lookups. Before or after examining the destination, other tables may be consulted to make decisions to drop the packet based on other considerations, such as the source address, the IP protocol identifier field, the Transmission Control Protocol (TCP), or User Datagram Protocol (UDP) port number.
Veriflow verifies the effect of rules on the network by slicing the network into a set of equivalence classes (ECs) of packets. Like an atomic flow, each EC is a set of packets that experience the same forwarding actions throughout the network. Veriflow takes advantage of the fact that each change to the network will typically only affect a small number of ECs to find the set of ECs whose operation could be altered by a rule and to verify network invariants only within those ECs. Veriflow also builds forwarding graphs for every modified EC to represent the network's forwarding behavior and traverses the forwarding graphs to determine the status of one or more invariants.
In operation, Veriflow verifies network properties by preparing a model of the entire network using its current data-plane state and runs queries on this model. For example, FIG. 1A illustrates an original network while FIG. 1B illustrates a network model as a data-plane higher level abstraction. As illustrated, the network elements are abstracted as switches (Tswitch) 10, routers (Trouter) 12, 14, firewalls (Tfirewall) 16, and MPLS devices (TMPLS) 18. The network is then sliced into a set of ECs based on the new rule and the existing rules that overlap the new rule. Veriflow implements a multi-dimensional prefix tree (trie) to store new network rules, to find overlapping rules, and to compute the affected ECs. A trie is an ordered tree data structure that stores an associative array. The trie associates the set of packets matched by a forwarding rule with the forwarding rule itself. Each level in the trie corresponds to a specific bit in a forwarding rule, which is equivalent to a bit in the packet header. Each node in the trie has three branches, corresponding to three possible values that the rule can match: 0, 1, and * (wildcard). The trie is characterized as a composition of several sub-tries or dimensions, each corresponding to a packet header field. A path from the trie's root to a leaf of one of the bottommost sub-tries represents a set of packets that a rule matches. Each leaf stores the rules that match that set of packets and the devices at which they are located.
When a new forwarding rule is generated by an application, a lookup in the trie is performed by traversing it dimension by dimension to find all the rules that intersect the new rule. At each dimension, the search area is narrowed down by only traversing those branches that fall within the range of the new rule using the field value of that particular dimension. The lookup procedure results in the selection of a set of leaves of the bottommost dimension, each with a set of forwarding rules. These rules collectively define a set of packets (in particular, their corresponding forwarding rules) that could be affected by the incoming forwarding rule. This set may span multiple ECs. For each field, a set of disjoint ranges (lower and upper bound) is found such that no rule splits one of the ranges. An EC is then defined by a particular choice of one of the ranges for each of the fields.
For each computed EC, Veriflow generates a forwarding graph. Each such graph is a representation of how packets within an EC will be forwarded through the network. In the graph, a node represents an EC at a particular network device, and a directed edge represents a forwarding decision for a particular EC or device pair. Specifically, an edge X→Y indicates that according to the forwarding table at node X, packets within this EC are forwarded to Y. To build the graph for each EC, the trie is traversed a second time to find the devices and rules that match packets from that EC. The second traversal is needed to find all those rules that were not necessary to compute the affected ECs in the first traversal, yet can still influence their forwarding behavior. In this fashion, Veriflow only has to traverse those branches of the trie having rules that can match packets of that particular EC.
Thus, Veriflow models the behavior of the network using forwarding graphs built only for those ECs whose behavior may have changed. The forwarding graphs are then used to check conditions concerning network behavior, such as reachability (whether packets will be delivered to the destination address specified in the rule), loop detection, consistency, “black holes” where packets are dropped, isolation, verification of access control policies, whether a new rule conflicts with an existing rule, whether an EC changes its next hop due to the insertion/deletion of a rule, whether a packet will always traverse a firewall, and the like.
However, the effectiveness of the Veriflow approach is limited by a number of factors including the complexity of the verification functions, the size of the network, the number of rules in the network, the number of unique ECs covered by a new rule, the number of header fields used to match packets by a new rule, and the like. The most important factor for verification time is the number of ECs modified. The verification time is roughly linearly related to the number of ECs modified, and Veriflow has difficulty verifying invariants in real-time when large portions of the network's forwarding behavior are altered in one operation. Thus, though Veriflow purports to verify network invariants in real-time, the Veriflow system is generally too slow to meet real-time network verification requirements in large-scale networks.